$\forall$$T$:Type, ${\it as}$,${\it bs}$:($T$ List), $i$:int\_seg(0; $\parallel$${\it as}$$\parallel$). append(${\it as}$; ${\it bs}$)[$i$] = ${\it as}$[$i$] $\in$ $T$